Inference at * 1 2 
Iof proof for Lemma l before antisymmetry:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. no_repeats(T;l)
6. [x; y]  l
7. [y; x]  l
8. [x; x]  l
  False 

latex

 by InteriorProof (AllHyps (\i. ((((((((((RWO "no_repeats_iff" i) 
CollapseTHEN (
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t
CollapseTHEN () inil_term)))) 
CollapseTHEN (Unfold `l_before` i))) 
CollapseTHEN (
CollapseTHEN (InstHyp [x;x] i))) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
CollapseTHEN ((Aut),(first_nat 4:n)) (first_tok :t) inil_term)))) 
CollapseTHEN (SimpHyp (-1))))
CollapseTHEN (Simp) 

latex

C.

Definitions	t  T, P & Q, P  Q, x before y  l, x:A. B(x), False, A, P  Q
Lemmas	no repeats iff